Section: New Results

Interfacing Coq with SMT solvers

Participants : Germain Faure, Chantal Keller [Contact] , Assia Mahboubi, Benjamin Werner.

This is work in close collaboration with the Marelle team (INRIA Sophia Antipolis). The starting point of this work is to note that SMT solvers, deciding the Satisfiability Modulo Theories, are in constant evolution to take into account new decision procedures as well as theories. These systems are rather complex and it is now clearly established that they all contain bugs. The standard approach is to ask the SMT solver to append to the decision result a certificate that can be checked by another tool.

In this context, we are using Coq to check the certificate. The approach is based on computational reflection. The checker is written in Coq , and its architecture is modular and extensible.

We are now able to check certificates coming from the ZChaff SAT solver and from the veriT SMT solver developed at INRIA Nancy – Grand - Est. Proofs established by the SMT tool for the theories of congruence closure and linear arithmetic are checked in short time, overtaking the state of the art in terms of time performance. We also use certificates to build a new Coq tactic that can safely call an external SMT solver, thus increasing Coq 's automation. This tactic is new since it is a decision procedure that combines both linear integer arithmetic and equality of uninterpreted functions. This work is described in a paper published in the proceedings of the CPP2011 conference [25] .